Invariant checking based on ordered binary decision diagrams (OBDDs) is a preferred method for checking assertions in the design of a circuit. OBDD-based invariant checking provides both falsification and verification, as opposed to bounded model checking (BMC) for example. This may be important, for example, in cases of abstraction refinement, where, after a series of false negatives and subsequent refinements, a property finally proves correct. OBBD-based invariant checking allows traversal in two directions: forward from initial states or backward from possible error states. One direction may provide significantly more efficient computation. As an example, one direction may reach a fixpoint in fewer steps. As another example, one direction may require significantly less computational complexity. However, a user does not know in advance which direction may provide more efficient computation.